$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). $P$ $\vee$ $P$ $\Leftarrow\!\Rightarrow$ $P$